D:Dsys, i:Id, s1, s2:M(i).state, k1, k2:Knd, v1:d-decl(D;i)(k1), v2:d-decl(D;i)(k2), m1,
m2:{m:M(i).Msg| source(mlnk(m)) = i } List.
<s1,doact(k1;v1),m1> = <s2,doact(k2;v2),m2>  d-world-state(D;i)
 s1 = s2 & k1 = k2 & v1 = v2  d-decl(D;i)(k1) & m1 = m2 

latex

Definitions	t  T, d-decl(D;i), Knd, x:A. B(x), x. t(x), 1of(t), 2of(t), Unit, P  Q, doact(k;v), Action(dec), M(i), M.Msg, Id, M.state, d-world-state(D;i), Dsys, mlnk(m), source(l), Prop, P & Q
Lemmas	d-world-state wf, ma-msg wf, lsrc wf, mlnk wf d, d-decl wf, Knd wf, ma-st wf, d-m wf, Id wf, dsys wf, doact wf, action wf, inr equal, unit wf, pi2 wf, pi1 wf